<!DOCTYPE html>
<html>
  <head>
    <meta charset="utf-8"> <meta name="viewport" content="width=device-width">
    <title>SAT问题的几种近似方法</title>
    <meta name="viewport" content="width=device-width,initial-scale=1, shrink-to-fit=no">
    <!-- Bootstrap CSS -->
    <link rel="stylesheet"
          href="https://cdn.jsdelivr.net/npm/bootstrap@4.5.0/dist/css/bootstrap.min.css"
          integrity="sha384-9aIt2nRpC12Uk9gS9baDl411NQApFmC26EwAOH8WgZl5MYYxFfc+NcPb1dKGj7Sk"
          crossorigin="anonymous">
    <link rel="stylesheet"
          href="//cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/styles/androidstudio.min.css">
<!--    <link rel="stylesheet" href="/web_template_css.css">-->
    <!-- this is highlight.js -->
    <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
    <script id="MathJax-script" async
            src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
    </script>
    <script  src="https://cdn.jsdelivr.net/npm/jquery@3.5.1/dist/jquery.slim.min.js"
    integrity="sha384-DfXdz2htPH0lsSSs5nCTpuj/zy4C+OGpamoFVy38MVBnE+IbbVYUew+OrCXaRkfj" crossorigin="anonymous"></script>
    <script src="https://cdn.jsdelivr.net/npm/popper.js@1.16.0/dist/umd/popper.min.js"
    integrity="sha384-Q6E9RHvbIyZFJoft+2mJbHaEWldlvI9IOYy5n3zV9zzTtmI3UksdQRVvoxMfooAo" crossorigin="anonymous"></script>
    <script src="https://cdn.jsdelivr.net/npm/bootstrap@4.5.0/dist/js/bootstrap.min.js"
    integrity="sha384-OgVRvuATP1z7JjHLkuOU7Xw704+h835Lr+6QL9UvYjZE3Ipu6Tp75j7Bh/kR0JKI" crossorigin="anonymous"></script>
    <script src="//cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/highlight.min.js"></script>
    <style>
      img{
        display: block;
        height: auto;
        max-width: 100%;
      }
    </style>
  </head>
  <body>
    <nav class="navbar navbar-expand-lg navbar-light bg-light">
        <a class="navbar-brand" href="#">kvrmnks</a>
        <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarNav" aria-controls="navbarNav" aria-expanded="false" aria-label="Toggle navigation">
          <span class="navbar-toggler-icon"></span>
        </button>
        <div class="collapse navbar-collapse" id="navbarNav">
          <ul class="navbar-nav">
            <li class="nav-item active">
              <a class="nav-link" href="./../../../../../index.html" target="_self">Home <span class="sr-only">(current)</span></a>
            </li>
            <li class="nav-item">
              <a class="nav-link" href="./../../../../../blog.html">Blog</a>
            </li>
            <li class="nav-item">
              <a class="nav-link" href="./../../../../../about.html">About</a>
            </li>
          </ul>
        </div>
      </nav>



    <div class='container'>
      <h1>Max-KSAT问题的几种近似方法</h1>

<h2>问题简介</h2>

<h3>SAT</h3>

<p>首先介绍一下SAT问题，首先假设大家都知道合取范式是什么(</p>

<p>不妨假设有\(n\)个布尔变量, \(m\)个析取范式.</p>

<p>根据命题逻辑理论, 合取范式可以表示成多个析取范式的合取, </p>

<p>而对于每个析取范式, 显然每个布尔变量的循序是无关的.</p>

<p>而且对于每个析取范式, 一个布尔变量出现多次, 也是没有意义的.</p>

<p>于是我们可以用一个集合来表示一个析取范式, 例如\(q_{1}\bigvee q_{2}\bigvee \hat{q_{3}}\), 其中\(\hat{q_{3}}\)表示\(q_{3}\)的否定形式.</p>

<p>我们就可以直接用集合\(\{q_{1}, q_{2}, \hat{q_{3}}\}\), 来表示.</p>

<p>于是SAT问题是, 能否有一个真值指派, 令\(m\)个析取范式真值全为真.</p>

<p>根据Cook&#39;s law, SAT\(\in\)NP-Complete.</p>

<h3>Max-SAT</h3>

<p>Max-SAT问题是SAT问题的优化形式, 即求解一个真值指派, 使得真值为真的析取范式数量最多.</p>

<p>显然SAT问题是Max-SAT的子问题, 所以Max-SAT\(\in\)NP.</p>

<p>于是只能考虑一些近似算法来达到很好的效果了.</p>

<h2>简单的Max-SAT近似算法</h2>

<p>先考虑一种很简单的贪心策略, 按照某一个顺序枚举布尔变量, 看看当前这个布尔变量选真可以满足的多还是选假满足的多.</p>

<p>首先来分析一发时间复杂度, 由于算法不复杂, 我就不出示代码了, 显然时间复杂度是\(O(n^2m)\)的, 假设通过数组实现每个集合, 总之是个多项式复杂度的算法. 比原来的指数级算法高到不知道哪里去了((</p>

<p>再来分析一波空间复杂度, 显然是\(O(nm)\) 的.</p>

<p>好了, 以上均是废话.</p>

<p>现在考虑这个算法的近似度上界.</p>

<p>考虑每一次选择中, 得到的一定比丢掉的多, 最坏情况下得到的和求掉的一样多, 所以可以猜测近似度上界为2, 然后归纳证明.</p>

<p>考虑对\(n\)施加归纳法, 当\(n\)为1时, 显然满足.</p>

<p>假设当\(n=k-1\)时满足, 考虑\(n=k\)时.</p>

<p>我们首先从\(k\)个布尔变量中随便选挑一个布尔变量, 不妨记这个布尔变量为\(x\), 按照上面的流程选择一个真值指派.</p>

<p>假设一共有\(m_{x}\)个析取范式中涉及了\(x\)或者\(\hat{x}\)变量, 那么我们最坏情况下能够令\(\frac{m_{x}}{2}\)个析取范式满足.</p>

<p>剩余\(m-\frac{m_{x}}{2}\)析取范式根据假设一定能够满足\(\frac{m-\frac{m_{x}}{2}}{2}\)个, 求一发和得到\(\frac{m+\frac{m_{x}}{2}}{2}&gt;\frac{m}{2}\), 显然最优算法最多使得\(m\)个析取范式得到满足.</p>

<p>于是很显然得到这个算法的近似上界为2.</p>

<p>这么简单的算法就能得到相当好的效果.</p>

<h2>Max-KSAT问题的简单近似算法1</h2>

<p>根据参数算法的思路, 我们可以通过找到更多的参数来对问题进行限制, 使得问题有更好的做法, 或是更好的近似方法.</p>

<p>Max-KSAT问题的含义是, 每个析取范式中至少存在\(k\)个布尔变量, 其余方面与Max-SAT问题相同.</p>

<p>很显然可以直接使用上面介绍的算法, 并可以把最后分析的放缩放缓一点.</p>

<p>回到**求一发和**的地方, 显然\(m_{x} \geq k\), 于是近似上界可以表示成\(\frac{2}{1+\frac{k}{2m}}\), 可以发现\(k\)越大近似上界越小.</p>

<h2>Max-KSAT问题的简单近似算法2</h2>

<p>现在考虑一种更加贪的做法, 不是按照一个随便的顺序尝试每个布尔变量, 而是直接每次找到可以满足最多项的布尔变量.</p>

<p>一种比较简单的实现方式下时间复杂度为\(O(n^3m)\), 空间复杂度为\(O(nm)\).</p>

<p>为了得到这个算法的近似上界, 维护两个集合(集群)\(A\), \(B\).</p>

<p>其中集群\(A\)维护当前已经满足的析取范式们, 集群\(B\)维护还没确定能不能满足的析取范式们, 当整个贪心程序结束时, 集群\(B\)就有了别的含义, 即不能满足的析取范式们, 而\(|A|\)便是这个简单近似算法给出的解.</p>

<p>现在正式开始分析这个近似算法的近似上界.</p>

<p>在贪每一个布尔变量时, 显然可以满足的析取范式的项数大于等于不能满足的析取范式的项数.</p>

<p>考虑累加这个不等式, 左边求和就是\(|A|\), 右边是不好求和, 但是可以找出一个下界是\(k|B|\)(因为已经考虑了每个布尔变量,所以最终不满足的析取范式中最少会在右边出现\(k\)次)</p>

<p>于是现在有了一个很强的不等式\(|A|\geq k|B|\), 此外还有\(|A|+|B|=m\)(没想到吧.jpg), 可以得到\(|A| \geq \frac{km}{1+k}\), 于是近似上界可以表示为\(\frac{k+1}{k}\)</p>

<p>不知道你有没有发现, 其实没必要每次找到可以满足最多项的布尔变量, 其实这个算法的本质和上个算法一样, 只不过是做到了更加精确的上界分析.</p>

<h2>Max-KSAT问题的不是那么简单的近似算法</h2>

<p>可以继续发挥人类智力得到更多的贪心策略.</p>

<p>考虑这样一种情况, 如果一个析取范式里的布尔变量元素很少, 或者更加精确的说, 还可以供分配的布尔变量个数很少, 这个时候应该尽量满足它们, 因为对于别的含有更多可供分配的布尔变量的析取范式, 有更多的机会被满足.</p>

<p>一些神仙想到了可以给每个析取范式加权, 来提高那些含有可供分配的布尔变量的析取范式被满足的机会.</p>

<p>定义一个权函数\(W(x) = 2^{-|x|}, x\in\) 析取范式集合. 特别的\(|x|\)表示\(x\)中可供分配的布尔变量的个数.</p>

<p>每贪一个布尔变量的时候, 对这个布尔变量取真时满足的析取范式的权函数求和, 同样对这个布尔变量取假时的满足的析取范式的权函数求和, 取一个大的集合.</p>

<p>沿用上面那个解法的记号\(A\), \(B\). </p>

<blockquote>
<p>其中集群\(A\)维护当前已经满足的析取范式们, 集群\(B\)维护还没确定能不能满足的析取范式们, 当整个贪心程序结束时, 集群\(B\)就有了别的含义, 即不能满足的析取范式们, 而\(|A|\)便是这个简单近似算法给出的解.</p>
</blockquote>

<p>首先分析初始状态下, \(B\)中集合权值和的大小一定小于\(\frac{m}{2^{k}}\), 每一步中在\(B\)中取走的集合的权值和一定大于等于没取走的集合的权值和, 于是在贪心过程中\(B\)中的集合权值和单调不增. 由于最后\(B\)中集合的权值都为\(1\), 所以有\(|B|\geq \frac{m}{2^{k}}\), 所有有近似上界为\(\frac{2^{k}}{2^{k}-1}\)</p>


    </div>
    <script>
      hljs.initHighlightingOnLoad()
    </script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/highlightjs-line-numbers.js/2.5.0/highlightjs-line-numbers.min.js"></script>
  <script>
      hljs.initHighlightingOnLoad();
      hljs.initLineNumbersOnLoad();
  </script>
  </body>
</html>